Inference at * 1 2 2 2 
Iof proof for Lemma sub-equality:



1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
7. P(i)
8. u  {j:T| P(j)} 
  {j:T| P(j)}  

latex

 by (UseWitness u) 
CollapseTHEN (Trivial) 

latex

C.

Definitions

t  T